home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / lib / h / ansi next >
Text File  |  1996-09-04  |  29KB  |  946 lines
  1. /*
  2. ** ansi.h --- LCLint Standard C Library
  3. **
  4. ** Process with -DSTRICT to get strict library.
  5. */
  6.  
  7. /*@-nextlinemacros@*/
  8. /*@+allimponly@*/
  9. /*@+globsimpmodifiesnothing@*/
  10.  
  11. /*
  12. ** errno.h
  13. */
  14.  
  15. /*@constant int EDOM;@*/
  16. /*@constant int ERANGE;@*/
  17. /*@constant int EILSEQ;@*/
  18.  
  19. # ifdef STRICT
  20. /*@checkedstrict@*/ extern int errno;
  21. # else 
  22. /*@unchecked@*/ extern int errno;
  23. # endif
  24.  
  25. /*
  26. ** types 
  27. */
  28.  
  29. typedef /*@integraltype@*/ ptrdiff_t;    
  30. typedef /*@unsignedintegraltype@*/ size_t;
  31. typedef /*@signedintegraltype@*/ ssize_t;
  32. typedef /*@integraltype@*/ wchar_t;
  33.  
  34. /*
  35. ** Added by Amendment 1 to ISO.
  36. */
  37.  
  38. typedef /*@integraltype@*/ wint_t;
  39. typedef /*@abstract@*/ mbstate_t;
  40.  
  41. /*@constant null anytype NULL = 0;@*/
  42.  
  43. /*
  44. ** assert.h
  45. */
  46.  
  47. /*@constant bool NDEBUG;@*/
  48.  
  49. # ifdef STRICT
  50. extern /*@falseexit@*/ void assert (/*@sef@*/ bool e) 
  51.   /*@*/ ;
  52. # else
  53. extern /*@falseexit@*/ void assert (/*@sef@*/ bool /*@alt int@*/ e) 
  54.   /*@*/ ;
  55. # endif
  56.  
  57.  
  58. /*
  59. ** ctype.h
  60. */
  61.  
  62. # ifdef STRICT
  63. extern bool isalnum (char c) /*@*/ ;
  64. extern bool isalpha (char c) /*@*/ ;
  65. extern bool iscntrl (char c) /*@*/ ;
  66. extern bool isdigit(char c) /*@*/ ;
  67. extern bool isgraph(char c) /*@*/ ;
  68. extern bool islower(char c) /*@*/ ;
  69. extern bool isprint(char c) /*@*/ ;
  70. extern bool ispunct(char c) /*@*/ ;
  71. extern bool isspace(char c) /*@*/ ;
  72. extern bool isupper(char c) /*@*/ ;
  73. extern bool isxdigit(char c) /*@*/ ;
  74. extern char tolower(char c) /*@*/ ;
  75. extern char toupper(char c) /*@*/ ;
  76. # else
  77. extern bool /*@alt int@*/ isalnum (char /*@alt int@*/ c) /*@*/ ;
  78. extern bool /*@alt int@*/ isalpha (char /*@alt int@*/ c) /*@*/ ;
  79. extern bool /*@alt int@*/ iscntrl (char /*@alt int@*/ c) /*@*/ ;
  80. extern bool /*@alt int@*/ isdigit(char /*@alt int@*/ c) /*@*/ ;
  81. extern bool /*@alt int@*/ isgraph(char /*@alt int@*/ c) /*@*/ ;
  82. extern bool /*@alt int@*/ islower(char /*@alt int@*/ c) /*@*/ ;
  83. extern bool /*@alt int@*/ isprint(char /*@alt int@*/ c) /*@*/ ;
  84. extern bool /*@alt int@*/ ispunct(char /*@alt int@*/ c) /*@*/ ;
  85. extern bool /*@alt int@*/ isspace(char /*@alt int@*/ c) /*@*/ ;
  86. extern bool /*@alt int@*/ isupper(char /*@alt int@*/ c) /*@*/ ;
  87. extern bool /*@alt int@*/ isxdigit(char /*@alt int@*/ c) /*@*/ ;
  88. extern char /*@alt int@*/ tolower(char /*@alt int@*/ c) /*@*/ ;
  89. extern char /*@alt int@*/ toupper(char /*@alt int@*/ c) /*@*/ ;
  90. # endif
  91.  
  92. /*
  93. ** locale.h
  94. */
  95.  
  96. struct lconv
  97. {
  98.   char *decimal_point;
  99.   char *thousands_sep;
  100.   char *grouping;
  101.   char *int_curr_symbol;
  102.   char *currency_symbol;
  103.   char *mon_decimal_point;
  104.   char *mon_thousands_sep;
  105.   char *mon_grouping;
  106.   char *positive_sign;
  107.   char *negative_sign;
  108.   char int_frac_digits;
  109.   char frac_digits;
  110.   char p_cs_precedes;
  111.   char p_sep_by_space;
  112.   char n_cs_precedes;
  113.   char n_sep_by_space;
  114.   char p_sign_posn;
  115.   char n_sign_posn;
  116. } ;
  117.  
  118. /*@constant int LC_ALL;@*/
  119. /*@constant int LC_COLLATE;@*/
  120. /*@constant int LC_CTYPE;@*/
  121. /*@constant int LC_MONETARY;@*/
  122. /*@constant int LC_NUMERIC;@*/
  123. /*@constant int LC_TIME;@*/
  124.  
  125. extern /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale) 
  126.    /*@modifies internalState, errno@*/ ;
  127.  
  128. extern struct lconv *localeconv (void) /*@*/ ;
  129.  
  130. /*
  131. ** float.h
  132. */
  133.  
  134. /*
  135. ** Note, these are defined by macros, but NOT necessarily
  136. ** constants.  They may be used as rvalues.
  137. */
  138.  
  139. /*@unchecked@*/ extern int    DBL_DIG;
  140. /*@unchecked@*/ extern double DBL_EPSILON;
  141. /*@unchecked@*/ extern int    DBL_MANT_DIG;
  142. /*@unchecked@*/ extern double DBL_MAX;
  143. /*@unchecked@*/ extern int    DBL_MAX_10_EXP;
  144. /*@unchecked@*/ extern int    DBL_MAX_EXP;
  145. /*@unchecked@*/ extern double DBL_MIN;
  146. /*@unchecked@*/ extern int    DBL_MIN_10_EXP;
  147. /*@unchecked@*/ extern int    DBL_MIN_EXP;
  148.  
  149. /*@unchecked@*/ extern int   FLT_DIG;
  150. /*@unchecked@*/ extern float FLT_EPSILON;
  151. /*@unchecked@*/ extern int   FLT_MANT_DIG;
  152. /*@unchecked@*/ extern float FLT_MAX;
  153. /*@unchecked@*/ extern int   FLT_MAX_10_EXP;
  154. /*@unchecked@*/ extern int   FLT_MAX_EXP;
  155. /*@unchecked@*/ extern float FLT_MIN;
  156. /*@unchecked@*/ extern int   FLT_MIN_10_EXP;
  157. /*@unchecked@*/ extern int   FLT_MIN_EXP;
  158. /*@constant            int   FLT_RADIX@*/
  159. /*@unchecked@*/ extern int   FLT_ROUNDS;
  160.  
  161. /*@unchecked@*/ extern int         LDBL_DIG;
  162. /*@unchecked@*/ extern long double LDBL_EPSILON;
  163. /*@unchecked@*/ extern int         LDBL_MANT_DIG;
  164. /*@unchecked@*/ extern long double LDBL_MAX;
  165. /*@unchecked@*/ extern int         LDBL_MAX_10_EXP;
  166. /*@unchecked@*/ extern int         LDBL_MAX_EXP;
  167. /*@unchecked@*/ extern long double LDBL_MIN;
  168. /*@unchecked@*/ extern int         LDBL_MIN_10_EXP;
  169. /*@unchecked@*/ extern int         LDBL_MIN_EXP;
  170.  
  171. /*
  172. ** limits.h
  173. */
  174.  
  175. /*@constant int CHAR_BIT; @*/
  176. /*@constant char CHAR_MAX; @*/
  177. /*@constant char CHAR_MIN; @*/
  178. /*@constant int INT_MAX; @*/
  179. /*@constant int INT_MIN; @*/
  180. /*@constant long int LONG_MAX; @*/
  181. /*@constant long int LONG_MIN; @*/
  182. /*@constant long int MB_LEN_MAX@*/
  183. /*@constant signed char SCHAR_MAX; @*/
  184. /*@constant signed char SCHAR_MIN; @*/
  185. /*@constant short SHRT_MAX; @*/
  186. /*@constant short SHRT_MIN; @*/
  187. /*@constant unsigned char UCHAR_MAX; @*/
  188. /*@constant unsigned char UCHAR_MIN; @*/
  189. /*@constant unsigned int UINT_MAX; @*/
  190. /*@constant unsigned long ULONG_MAX; @*/
  191. /*@constant unsigned short USHRT_MAX; @*/
  192.  
  193. /*
  194. ** math.h
  195. */
  196.  
  197. /*@constant double HUGE_VAL; @*/
  198.  
  199. /*
  200. ** math functions that may have a range error modify errno 
  201. */
  202.  
  203. extern double sin (double x) /*@*/ ;
  204. extern double cos (double x) /*@*/ ;
  205. extern double tan (double x) /*@*/ ;
  206. extern double asin (double x) /*@modifies errno@*/ ;
  207. extern double acos (double x) /*@modifies errno@*/ ;
  208. extern double atan (double x) /*@*/ ;
  209. extern double atan2 (double y, double x) /*@*/ ;
  210. extern double sinh (double x) /*@*/ ;
  211. extern double cosh (double x) /*@modifies errno@*/ ;
  212. extern double tanh (double x) /*@*/ ;
  213.  
  214. extern double exp (double x) /*@modifies errno@*/ ;
  215. extern double ldexp (double x, int n) /*@modifies errno@*/ ;
  216. extern double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
  217.  
  218. extern double log (double x) /*@modifies errno@*/ ;
  219. extern double log10 (double x) /*@modifies errno@*/ ;
  220.  
  221. extern double pow (double x, double y) /*@modifies errno@*/ ;
  222. extern double sqrt (double x) /*@modifies errno@*/ ;
  223.  
  224. extern double ceil (double x) /*@*/ ;
  225. extern double floor (double x) /*@*/ ;
  226. extern double fabs (double x) /*@*/ ;
  227.  
  228. double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
  229. double fmod (double x, double y) /*@*/ ;
  230.  
  231. /*
  232. ** These functions are optional in iso C.  An implementation does not
  233. ** have to provide them.  They are included in comments here, but
  234. ** are not required to be part of the standard library.
  235. */
  236.  
  237. # ifdef OPTIONAL_MATH
  238.  
  239. extern float acosf (float x) /*@modifies errno@*/ ;
  240. extern long double acosl (long double x) /*@modifies errno@*/ ;
  241. extern float asinf (float x)    /*@modifies errno@*/ ;
  242. extern long double asinl (long double x) /*@modifies errno@*/ ;
  243. extern float atanf (float x)    /*@*/ ;
  244. extern long double atanl (long double x) /*@*/ ;
  245. extern float atan2f (float y, float x) /*@*/ ;
  246. extern long double atan2l (long double y, long double x) /*@*/ ;
  247. extern float ceilf (float x)    /*@*/ ;
  248. extern long double ceill (long double x) /*@*/ ;
  249. extern float cosf (float x) /*@*/ ;
  250. extern long double cosl (long double x) /*@*/ ;
  251. extern float coshf (float x)    /*@modifies errno@*/ ;
  252. extern long double coshl (long double x) /*@modifies errno@*/ ;
  253. extern float expf (float x) /*@modifies errno@*/ ;
  254. extern long double expl (long double x) /*@modifies errno@*/;
  255. extern float fabsf (float x)    /*@*/ ;
  256. extern long double fabsl (long double x) /*@*/ ;
  257. extern float floorf (float x) /*@*/ ;
  258. extern long double floorl (long double x) /*@*/ ;
  259. extern float fmodf (float x, float y) /*@*/ ;
  260. extern long double fmodl (long double x, long double y)    /*@*/ ;
  261. extern float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/;
  262. extern long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/;
  263. extern float ldexpf (float x, int n) /*@modifies errno@*/ ;
  264. extern long double ldexpl (long double x, int n) /*@modifies errno@*/ ;
  265. extern float logf (float x) /*@modifies errno@*/ ;
  266. extern long double logl (long double x) /*@modifies errno@*/ ;
  267. extern float log10f (float x) /*@modifies errno@*/;
  268. extern long double log10l (long double x) /*@modifies errno@*/;
  269. extern float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ;
  270. extern long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ;
  271. extern float powf (float x, float y) /*@modifies errno@*/ ;
  272. extern long double powl (long double x, long double y) /*@modifies errno@*/ ;
  273. extern float sinf (float x) /*@*/ ;
  274. extern long double sinl (long double x)    /*@*/ ;
  275. extern float sinhf (float x) /*@*/ ;
  276. extern long double sinhl (long double x) /*@*/ ;
  277. extern float sqrtf (float x) /*@modifies errno@*/ ;
  278. extern long double sqrtl (long double x) /*@modifies errno@*/ ;
  279. extern float tanf (float x) /*@*/ ;
  280. extern long double tanl (long double x)    /*@*/ ;
  281. extern float tanhf (float x) /*@*/ ;
  282. extern long double tanhl (long double x) /*@*/ ;
  283.  
  284. # endif
  285.  
  286. /*
  287. ** setjmp.h
  288. */
  289.  
  290. typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
  291.  
  292. extern int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
  293. extern /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
  294.  
  295. /*
  296. ** signal.h
  297. */
  298.  
  299. /*@constant int SIGABRT; @*/
  300. /*@constant int SIGFPE; @*/
  301. /*@constant int SIGILL; @*/
  302. /*@constant int SIGINT; @*/
  303. /*@constant int SIGSEGV; @*/
  304. /*@constant int SIGTERM; @*/
  305.  
  306. typedef /*@integraltype@*/ sig_atomic_t;
  307.  
  308. /*@constant void (*SIG_DFL)(int); @*/
  309. /*@constant void (*SIG_ERR)(int); @*/
  310. /*@constant void (*SIG_IGN)(int); @*/
  311.  
  312. extern void (*signal) (int sig, /*@null@*/ void (*func)(int)) 
  313.    /*@modifies internalState, errno;@*/ ;
  314.  
  315. extern /*@mayexit@*/ int raise (int sig) ;
  316.  
  317. /*
  318. ** stdarg.h
  319. */
  320.  
  321. typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
  322.  
  323. extern void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
  324. extern void va_end (va_list va) /*@modifies va;@*/ ;
  325.  
  326. /*
  327. ** va_arg is builtin
  328. */
  329.  
  330. /*
  331. ** stdio.h
  332. */
  333.  
  334. typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
  335. typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
  336.  
  337. /*@constant int _IOFBF; @*/
  338. /*@constant int _IOLBF; @*/
  339. /*@constant int _IONBF; @*/
  340.  
  341. /*@constant int BUFSIZ; @*/
  342. /*@constant int EOF; @*/
  343.  
  344. /*@constant int FOPEN_MAX; @*/
  345. /*@constant int FILENAME_MAX; @*/
  346.  
  347. /*@constant int L_tmpnam; @*/
  348.  
  349. /*@constant int SEEK_CUR; @*/
  350. /*@constant int SEEK_END; @*/
  351. /*@constant int SEEK_SET; @*/
  352.  
  353. /*@constant int TMP_MAX; @*/
  354.  
  355. # ifdef STRICT
  356. /*@checked@*/ FILE *stderr;
  357. /*@checked@*/ FILE *stdin;
  358. /*@checked@*/ FILE *stdout;
  359. # else
  360. /*@unchecked@*/ FILE *stderr;
  361. /*@unchecked@*/ FILE *stdin;
  362. /*@unchecked@*/ FILE *stdout;
  363. # endif
  364.  
  365. extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
  366. extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
  367.  
  368. extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
  369. extern /*@observer@*/ char *
  370.   tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) 
  371.   /*@modifies *s, internalState@*/ ;
  372.  
  373. extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
  374. extern int fflush (/*@null@*/ FILE *stream) 
  375.    /*@modifies *stream, errno, fileSystem;@*/ ;
  376.  
  377. extern /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) 
  378.    /*@modifies fileSystem@*/ ;         
  379.  
  380. extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) 
  381.   /*@modifies *stream, fileSystem, errno@*/ ;
  382.  
  383. extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf) 
  384.    /*@modifies fileSystem, *stream, *buf@*/ ;
  385.  
  386. extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, 
  387.             int mode, size_t size)
  388.    /*@modifies fileSystem, *stream, *buf@*/ ;
  389.  
  390. # ifdef STRICT
  391. /*@printflike@*/ 
  392. extern int fprintf (FILE *stream, char *format, ...)
  393.    /*@modifies fileSystem, *stream@*/ ;
  394. # else
  395. /*@printflike@*/ 
  396. extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
  397.    /*@modifies fileSystem, *stream@*/ ;
  398. # endif
  399.  
  400. /*@scanflike@*/ 
  401. extern int fscanf (FILE *stream, char *format, ...)
  402.    /*@modifies fileSystem, *stream@*/ ;
  403.  
  404. # ifdef STRICT
  405. /*@printflike@*/ 
  406. extern int printf (char *format, ...) 
  407.    /*@globals stdout@*/
  408.    /*@modifies fileSystem, *stdout@*/ ;
  409. # else
  410. /*@printflike@*/ 
  411. extern int /*@alt void@*/ printf (char *format, ...) 
  412.    /*@globals stdout@*/
  413.    /*@modifies fileSystem, *stdout@*/ ;
  414. # endif
  415.  
  416. /*@scanflike@*/
  417. extern int scanf(char *format, ...)
  418.    /*@globals stdin@*/
  419.    /*@modifies fileSystem, *stdin@*/ ;
  420.  
  421. # ifdef STRICT
  422. /*@printflike@*/ 
  423. extern int sprintf (/*@out@*/ char *s, char *format, ...) 
  424.    /*@modifies *s@*/ ;
  425. # else
  426. /*@printflike@*/ 
  427. extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) 
  428.    /*@modifies *s@*/ ;
  429. # endif
  430.  
  431. /*@scanflike@*/ 
  432. int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
  433.    /* modifies extra arguments */
  434.  
  435. extern int vfprintf (FILE *stream, char *format, va_list arg)
  436.    /*@modifies fileSystem, *stream, arg, errno@*/ ;
  437.  
  438. extern int vprintf (char *format, va_list arg)
  439.    /*@globals stdout@*/
  440.    /*@modifies fileSystem, arg, *stdout@*/ ;
  441.  
  442. extern int vsprintf (/*@out@*/ char *s, char *format, va_list arg)
  443.    /*@modifies *s, arg@*/ ;
  444.  
  445. extern int fgetc (FILE *stream) 
  446.    /*@modifies fileSystem, *stream, errno@*/ ;
  447.  
  448. extern /*@null@*/ char *
  449.   fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
  450.   /*@modifies fileSystem, *s, *stream, errno@*/ ;
  451.  
  452. extern int fputc (int /*@alt char@*/ c, FILE *stream)
  453.   /*@modifies fileSystem, *stream, errno@*/ ;
  454.  
  455. extern int fputs (char *s, FILE *stream)
  456.   /*@modifies fileSystem, *stream@*/ ;
  457.  
  458. /* note use of sef --- stream may be evaluated more than once */
  459. extern int getc (/*@sef@*/ FILE *stream)
  460.   /*@modifies fileSystem, *stream@*/ ;
  461.  
  462. extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
  463.  
  464. extern /*@null@*/ char *gets (/*@out@*/ char *s) 
  465.    /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
  466.  
  467. extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
  468.   /*@modifies fileSystem, *stream;@*/ ;
  469.  
  470. extern int putchar (int /*@alt char@*/ c)
  471.    /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; 
  472.  
  473. extern int puts (const char *s)
  474.    /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; 
  475.  
  476. extern int ungetc (int /*@alt char@*/ c, FILE *stream)
  477.   /*@modifies fileSystem, *stream, errno@*/ ;
  478.  
  479. extern size_t 
  480.   fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
  481.   /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
  482.  
  483. extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
  484.   /*@modifies fileSystem, *stream, errno@*/ ;
  485.  
  486. extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
  487.   /*@modifies *pos, errno@*/ ;
  488.  
  489. extern int fseek (FILE *stream, long int offset, int whence)
  490.   /*@modifies fileSystem, *stream, errno@*/ ;
  491.  
  492. extern int fsetpos (FILE *stream, fpos_t *pos)
  493.    /*@modifies fileSystem, *stream, errno@*/ ;
  494.  
  495. extern long int ftell(FILE *stream) /*@modifies errno@*/ ;
  496.  
  497. extern void rewind (FILE *stream) /*@modifies *stream@*/ ;
  498. extern void clearerr (FILE *stream) /*@modifies *stream@*/ ;
  499.  
  500. extern int feof (FILE *stream) /*@modifies errno@*/ ;
  501. extern int ferror (FILE *stream) /*@modifies errno@*/ ;
  502.  
  503. extern void perror (/*@null@*/ char *s) 
  504.    /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; 
  505.  
  506. /*
  507. ** stdlib.h
  508. */
  509.  
  510. extern double atof (char *s) /*@*/ ;
  511. extern int atoi (char *s) /*@*/ ;
  512. extern long int atol (char *s) /*@*/ ;
  513.  
  514. extern double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
  515.   /*@modifies *endp, errno@*/ ;
  516.  
  517. extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
  518.   /*@modifies *endp, errno@*/ ;
  519.  
  520. extern unsigned long 
  521.   strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
  522.   /*@modifies *endp, errno@*/ ;
  523.  
  524. /*@constant int RAND_MAX; @*/
  525. extern int rand (void) /*@modifies internalState@*/ ;
  526. extern void srand (unsigned int seed) /*@modifies internalState@*/ ;
  527.  
  528. extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/ ;
  529. extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/ ;
  530. extern /*@null@*/ /*@out@*/ /*@only@*/ void *
  531.    realloc (/*@null@*/ /*@out@*/ /*@only@*/ /*@returned@*/ void *p, 
  532.         size_t size) /*@modifies *p@*/ ;
  533.  
  534. extern void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ ;
  535.  
  536. /*@constant int EXIT_FAILURE; @*/ 
  537. /*@constant int EXIT_SUCCESS; @*/ 
  538.  
  539. extern /*@exits@*/ void abort (void) /*@*/ ;
  540. extern /*@exits@*/ void exit (int status) /*@*/ ;
  541. extern int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
  542.  
  543. extern /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
  544.  
  545. extern int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
  546.  
  547. extern /*@null@*/ void *
  548.   bsearch (void *key, void *base, 
  549.        size_t n, size_t size, 
  550.        int (*compar)(void *, void *)) /*@*/ ;
  551.  
  552. extern void qsort (void *base, size_t n, size_t size, 
  553.            int (*compar)(void *, void *))
  554.    /*@modifies *base, errno@*/ ;
  555.  
  556. extern int abs (int n) /*@*/ ;
  557.  
  558. typedef /*@concrete@*/ struct 
  559. {
  560.   int quot;
  561.   int rem;
  562. } div_t ;
  563.  
  564. extern div_t div (int num, int denom) /*@*/ ;
  565.  
  566. extern long int labs (long int n) /*@*/ ; 
  567.  
  568. typedef /*@concrete@*/ struct 
  569. {
  570.   long int quot;
  571.   long int rem;
  572. } ldiv_t ;
  573.  
  574. extern ldiv_t ldiv (long num, long denom) /*@*/ ;
  575.  
  576. /*@constant size_t MB_CUR_MAX; @*/
  577.  
  578. /*
  579. ** wchar_t and wint_t functions added by Amendment 1 to ISO.
  580. */
  581.  
  582. /*@constant int WCHAR_MAX@*/
  583. /*@constant int WCHAR_MIN@*/
  584. /*@constant wint_t WEOF@*/
  585.  
  586. extern wint_t btowc (int c) /*@*/ ;
  587.  
  588. extern wint_t fgetwc (FILE *fp)    /*@modifies fileSystem, *fp*/ ;
  589.  
  590. extern /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
  591.    /*@modifies fileSystem, *s, *stream@*/;
  592.  
  593. extern wint_t fputwc (wchar_t c, FILE *stream)
  594.    /*@modifies fileSystem, *stream@*/;
  595.  
  596. extern int fputws (const wchar_t *s, FILE *stream)
  597.    /*@modifies fileSystem, *stream@*/ ;
  598.  
  599. extern int fwide (FILE *stream, int mode) /*@*/ ; 
  600.    /* does not modify the stream */
  601.  
  602. /*@printflike@*/ extern int fwprintf (FILE *stream, const wchar_t *format, ...)
  603.     /*@modifies *stream, fileSystem@*/ ;
  604.  
  605. /*@scanflike@*/ extern int fwscanf (FILE *stream, const wchar_t *format, ...)
  606.     /*@modifies *stream, fileSystem@*/ ;
  607.  
  608. /* note use of sef --- stream may be evaluated more than once */
  609. extern wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
  610.  
  611. extern wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
  612.  
  613. extern size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
  614.  
  615. extern size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
  616.                /*@null@*/ mbstate_t *ps) 
  617.    /*@modifies *pwc@*/ ;
  618.  
  619. extern int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
  620.  
  621. extern size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
  622.              /*@null@*/ mbstate_t *ps) 
  623.    /*@modifies *dst@*/ ;
  624.  
  625. /* note use of sef --- stream may be evaluated more than once */
  626. extern wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream)    /*@modifies fileSystem, *stream@*/ ;
  627.  
  628. extern wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
  629.  
  630. /*@printflike@*/ extern int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
  631.    /*@modifies *s@*/ ;
  632.  
  633. /*@scanflike@*/ extern int swscanf (const wchar_t *s, const wchar_t *format, ...)
  634.    /*@modifies *stdin@*/ ;
  635.  
  636. extern wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
  637.  
  638. extern int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
  639.    /*@modifies fileSystem, *stream@*/ ;
  640.  
  641. extern int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
  642.    /*@modifies *s@*/ ;
  643.  
  644. extern int vwprintf (const wchar_t *format, va_list arg)
  645.    /*@modifies fileSystem, *stdout@*/ ;
  646.  
  647. extern size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
  648.    /*@modifies *s@*/;
  649.  
  650. extern void /*@alt wchar_t *@*/
  651.   wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
  652.   /*@modifies *s1@*/ ;
  653.  
  654. extern /*@exposed@*/ /*@null@*/ wchar_t *
  655.   wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
  656.   /*@*/ ;
  657.  
  658. extern int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  659.  
  660. extern int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  661.  
  662. extern void /*@alt wchar_t *@*/ 
  663.   wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
  664.   /*@modifies *s1@*/ ;
  665.  
  666. extern size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  667.  
  668. extern size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
  669.             const struct tm *timeptr) 
  670.    /*@modifies *s@*/ ;
  671.  
  672. extern size_t wcslen (const wchar_t *s) /*@*/ ;
  673.  
  674. extern void /*@alt wchar_t *@*/
  675.   wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
  676.        size_t n) 
  677.   /*@modifies *s1@*/ ;
  678.  
  679. extern int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
  680.  
  681. extern void /*@alt wchar_t *@*/
  682.   wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
  683.        size_t n) 
  684.    /*@modifies *s1@*/ ;
  685.  
  686. extern /*@null@*/ wchar_t *
  687.   wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
  688.   /*@*/ ;
  689.  
  690. extern /*@null@*/ wchar_t *
  691.   wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
  692.   /*@*/ ;
  693.  
  694. extern size_t
  695.   wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
  696.          /*@null@*/ mbstate_t *ps) 
  697.   /*@modifies *src@*/ ;
  698.  
  699. extern size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  700.  
  701. extern /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  702.  
  703. extern double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
  704.    /*@modifies *endptr@*/ ;
  705.  
  706. extern /*@null@*/ wchar_t *
  707.   wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
  708.   /*@modifies *ptr@*/;
  709.  
  710. extern long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
  711.    /*@modifies *endptr@*/;
  712.  
  713. extern unsigned long
  714.   wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
  715.   /*@modifies *endptr@*/;
  716.  
  717. extern size_t
  718.   wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  719.   /*@modifies *s1@*/;
  720.  
  721. extern int wctob (wint_t c) /*@*/;
  722.  
  723. extern /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
  724.  
  725. extern int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
  726.  
  727. extern wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  728.    /*@modifies *s1@*/;
  729.  
  730. extern wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  731.    /*@modifies *s1@*/;
  732.  
  733. extern wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
  734.    /*@modifies *s@*/;
  735.  
  736. /*@printflike@*/ extern int wprintf (const wchar_t *format, ...)
  737.    /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
  738.  
  739. /*@scanflike@*/ extern int
  740.   wscanf (const wchar_t *format, ...)
  741.   /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
  742.  
  743. /*
  744. ** wctype.h (added by Amendment 1)
  745. */
  746.  
  747. /* Warning: not sure about these (maybe abstract?): */
  748. typedef /*@integraltype@*/ wctype_t;
  749. typedef /*@integraltype@*/ wctrans_t;
  750.  
  751. # ifdef STRICT
  752. extern bool iswalnum (wint_t c) /*@*/ ;
  753. extern bool iswalpha (wint_t c) /*@*/ ;
  754. extern bool iswcntrl (wint_t c) /*@*/ ;
  755. extern bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
  756. extern bool iswdigit (wint_t c) /*@*/ ;
  757. extern bool iswgraph (wint_t c) /*@*/ ;
  758. extern bool iswlower (wint_t c) /*@*/ ;
  759. extern bool iswprint (wint_t c) /*@*/ ;
  760. extern bool iswpunct (wint_t c) /*@*/ ;
  761. extern bool iswspace (wint_t c) /*@*/ ;
  762. extern bool iswupper (wint_t c) /*@*/ ;
  763. extern bool iswxdigit (wint_t c) /*@*/ ;
  764.  
  765. extern wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
  766. extern wint_t towlower (wint_t c) /*@*/ ;
  767. extern wint_t towupper (wint_t c) /*@*/ ;
  768. # else
  769. extern bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
  770. extern bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
  771. extern bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
  772. extern bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
  773. extern bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
  774. extern bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
  775. extern bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
  776. extern bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
  777. extern bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
  778. extern bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
  779. extern bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
  780. extern bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
  781.  
  782. extern wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg)    /*@*/ ;
  783. extern wint_t /*@alt int@*/ towlower (wint_t c)    /*@*/ ;
  784. extern wint_t /*@alt int@*/ towupper (wint_t c)    /*@*/ ;
  785. # endif
  786.  
  787. extern wctrans_t wctrans (const char *property)    /*@*/ ;
  788. extern wctype_t wctype (const char *property) /*@*/ ;
  789.  
  790. extern int mblen (char *s, size_t n) /*@*/ ;
  791. extern int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) 
  792.    /*@modifies *pwc@*/ ;
  793. extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) 
  794.    /*@modifies *s@*/ ;
  795. extern size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
  796.   /*@modifies *pwcs@*/ ;
  797. extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
  798.   /*@modifies *s@*/ ;
  799.  
  800. /*
  801. ** string.h
  802. */
  803.      
  804. extern void /*@alt void * @*/
  805.   memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) 
  806.   /*@modifies *s1@*/ ;
  807.  
  808. extern void /*@alt void * @*/
  809.   memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
  810.   /*@modifies *s1@*/ ;
  811.  
  812. extern void /*@alt char * @*/
  813.   strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2) 
  814.   /*@modifies *s1@*/ ;
  815.  
  816. extern void /*@alt char * @*/
  817.   strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n) 
  818.   /*@modifies *s1@*/ ;
  819.  
  820. extern void /*@alt char * @*/
  821.   strcat (/*@unique@*/ /*@returned@*/ /*@out@*/ char *s1, char *s2) 
  822.   /*@modifies *s1@*/ ;
  823.  
  824. extern void /*@alt char * @*/
  825.   strncat (/*@unique@*/ /*@returned@*/ /*@out@*/ char *s1, char *s2, int n)
  826.   /*@modifies *s1@*/ ;
  827.  
  828. extern int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
  829. extern int strcmp (char *s1, char *s2) /*@*/ ;
  830. extern int strcoll (char *s1, char *s2) /*@*/ ;
  831. extern int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
  832. extern size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n) 
  833.   /*@modifies *s1@*/ ;  /* s1 may be null only if n == 0 */ 
  834.  
  835. extern /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
  836.  
  837. # ifdef STRICT
  838. extern /*@exposed@*/ /*@null@*/ char *
  839.   strchr (/*@returned@*/ char *s, char c) /*@*/ ;
  840. # else
  841. extern /*@exposed@*/ /*@null@*/ char *
  842.   strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ ;
  843. # endif
  844.  
  845. extern size_t strcspn (char *s1, char *s2) /*@*/ ;
  846. extern /*@null@*/ /*@exposed@*/ char *
  847.   strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
  848.  
  849. # ifdef STRICT
  850. extern /*@null@*/ /*@exposed@*/ char *
  851.   strrchr (/*@returned@*/ char *s, char c) /*@*/ ;
  852. # else
  853. extern /*@null@*/ /*@exposed@*/ char *
  854.   strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ ;
  855. # endif
  856.  
  857. extern size_t strspn (char *s, char *t) /*@*/ ;
  858. extern /*@null@*/ /*@exposed@*/  char *
  859.   strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/ ; 
  860. extern /*@null@*/ /*@exposed@*/ char *
  861.   strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
  862.   /*@modifies *s, internalState, errno@*/ ;
  863.  
  864. extern void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s, 
  865.                      int c, size_t n)
  866.    /*@modifies *s@*/ ;
  867.  
  868. extern /*@observer@*/ char *strerror (int errnum) /*@*/ ;
  869.  
  870. extern size_t strlen (char *s) /*@*/ ; 
  871.  
  872. /*
  873. ** time.h
  874. */
  875.  
  876. /*@constant int CLOCKS_PER_SEC;@*/
  877.  
  878. typedef /*@integraltype@*/ clock_t;
  879. typedef /*@integraltype@*/ time_t;
  880.  
  881. struct tm
  882.   {
  883.     int tm_sec;
  884.     int tm_min;
  885.     int tm_hour;
  886.     int tm_mday;
  887.     int tm_mon;
  888.     int tm_year;
  889.     int tm_wday;
  890.     int tm_yday;
  891.     int tm_isdst;
  892.   } ;
  893.  
  894. extern clock_t clock (void) /*@modifies internalState@*/ ;
  895. extern double difftime (time_t time1, time_t time0) /*@*/ ;
  896. extern time_t mktime (struct tm *timeptr) /*@*/ ;
  897.  
  898. extern time_t time (/*@null@*/ /*@out@*/ time_t *tp)
  899.   /*@modifies *tp@*/ ;
  900.  
  901. extern /*@observer@*/ char *asctime (struct tm *timeptr) 
  902.   /*@modifies errno*/ ;
  903.  
  904. extern /*@observer@*/ char *ctime (time_t *tp) /*@*/ ;
  905.  
  906. extern /*@null@*/ /*@only@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
  907.  
  908. extern /*@null@*/ /*@only@*/ struct tm *localtime (time_t *tp) 
  909.   /*@modifies errno@*/ ;
  910.  
  911. extern size_t strftime (/*@out@*/ char *s, size_t smax,
  912.             char *fmt, struct tm *timeptr)
  913.   /*@modifies *s@*/ ;
  914.  
  915. /*
  916. ** These were added by Amendment 1.  Not all implementations provide these yet.
  917. ** Hmmm...what is the correct type of and_eq?
  918.  
  919. extern bool /*@alt int@*/ and_eq (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  920. extern bool /*@alt int@*/ not_eq (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  921. extern bool /*@alt int@*/ or_eq (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  922. extern bool /*@alt int@*/ xor_eq (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  923. */
  924.  
  925. # ifndef STRICT
  926. extern bool /*@alt int@*/ and (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  927.  
  928. extern int bitand (int, int) /*@*/ ;
  929. extern int bitor (int, int) /*@*/ ;
  930.  
  931. extern bool /*@alt int@*/ not (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  932. extern bool /*@alt int@*/ or (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  933. extern bool /*@alt int@*/ xor (bool /*@alt int@*/, bool /*@alt int@*/) /*@*/ ;
  934. # else
  935. extern bool and (bool, bool) /*@*/ ;
  936.  
  937. extern int bitand (int, int) /*@*/ ;
  938. extern int bitor (int, int) /*@*/ ;
  939.  
  940. extern bool not (bool, bool) /*@*/ ;
  941. extern bool or (bool, bool) /*@*/ ;
  942. extern bool xor (bool, bool) /*@*/ ;
  943. # endif
  944.  
  945.  
  946.